The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(O(1), O(n^1)).

0 CpxTRS
↳1 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID), 0 ms)
↳2 CdtProblem
    ↳3 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 41 ms)
    ↳4 CdtProblem
    ↳5 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳6 CdtProblem
    ↳7 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳8 CdtProblem
    ↳9 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳10 CdtProblem
    ↳11 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳12 CdtProblem
    ↳13 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳14 CdtProblem
    ↳15 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳16 CdtProblem
    ↳17 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳18 CdtProblem
    ↳19 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳20 CdtProblem
    ↳21 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳22 CdtProblem
↳23 CpxTrsMatchBoundsTAProof (⇔, 0 ms)
↳24 BOUNDS(O(1), O(n^1))

(0) Obligation:

Runtime Complexity TRS:
The TRS R consists of the following rules:

a(a(f(b, a(x)))) → f(a(a(a(x))), b)
a(a(x)) → f(b, a(f(a(x), b)))
f(a(x), b) → f(b, a(x))

Rewrite Strategy: INNERMOST

(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)

Converted CpxTRS to CDT

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

a(a(f(b, a(z0)))) → f(a(a(a(z0))), b)
a(a(z0)) → f(b, a(f(a(z0), b)))
f(a(z0), b) → f(b, a(z0))
Tuples:

A(a(f(b, a(z0)))) → c(F(a(a(a(z0))), b), A(a(a(z0))), A(a(z0)), A(z0))
A(a(z0)) → c1(F(b, a(f(a(z0), b))), A(f(a(z0), b)), F(a(z0), b), A(z0))
F(a(z0), b) → c2(F(b, a(z0)), A(z0))
S tuples:

A(a(f(b, a(z0)))) → c(F(a(a(a(z0))), b), A(a(a(z0))), A(a(z0)), A(z0))
A(a(z0)) → c1(F(b, a(f(a(z0), b))), A(f(a(z0), b)), F(a(z0), b), A(z0))
F(a(z0), b) → c2(F(b, a(z0)), A(z0))
K tuples:none
Defined Rule Symbols:

a, f

Defined Pair Symbols:

A, F

Compound Symbols:

c, c1, c2

(3) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace A(a(f(b, a(z0)))) → c(F(a(a(a(z0))), b), A(a(a(z0))), A(a(z0)), A(z0)) by

A(a(f(b, a(x0)))) → c(F(f(b, a(f(a(a(x0)), b))), b), A(a(a(x0))), A(a(x0)), A(x0))
A(a(f(b, a(f(b, a(z0)))))) → c(F(a(f(a(a(a(z0))), b)), b), A(a(a(f(b, a(z0))))), A(a(f(b, a(z0)))), A(f(b, a(z0))))
A(a(f(b, a(z0)))) → c(F(a(f(b, a(f(a(z0), b)))), b), A(a(a(z0))), A(a(z0)), A(z0))
A(a(f(b, a(x0)))) → c

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

a(a(f(b, a(z0)))) → f(a(a(a(z0))), b)
a(a(z0)) → f(b, a(f(a(z0), b)))
f(a(z0), b) → f(b, a(z0))
Tuples:

A(a(z0)) → c1(F(b, a(f(a(z0), b))), A(f(a(z0), b)), F(a(z0), b), A(z0))
F(a(z0), b) → c2(F(b, a(z0)), A(z0))
A(a(f(b, a(x0)))) → c(F(f(b, a(f(a(a(x0)), b))), b), A(a(a(x0))), A(a(x0)), A(x0))
A(a(f(b, a(f(b, a(z0)))))) → c(F(a(f(a(a(a(z0))), b)), b), A(a(a(f(b, a(z0))))), A(a(f(b, a(z0)))), A(f(b, a(z0))))
A(a(f(b, a(z0)))) → c(F(a(f(b, a(f(a(z0), b)))), b), A(a(a(z0))), A(a(z0)), A(z0))
A(a(f(b, a(x0)))) → c
S tuples:

A(a(z0)) → c1(F(b, a(f(a(z0), b))), A(f(a(z0), b)), F(a(z0), b), A(z0))
F(a(z0), b) → c2(F(b, a(z0)), A(z0))
A(a(f(b, a(x0)))) → c(F(f(b, a(f(a(a(x0)), b))), b), A(a(a(x0))), A(a(x0)), A(x0))
A(a(f(b, a(f(b, a(z0)))))) → c(F(a(f(a(a(a(z0))), b)), b), A(a(a(f(b, a(z0))))), A(a(f(b, a(z0)))), A(f(b, a(z0))))
A(a(f(b, a(z0)))) → c(F(a(f(b, a(f(a(z0), b)))), b), A(a(a(z0))), A(a(z0)), A(z0))
A(a(f(b, a(x0)))) → c
K tuples:none
Defined Rule Symbols:

a, f

Defined Pair Symbols:

A, F

Compound Symbols:

c1, c2, c, c

(5) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

Removed 1 trailing nodes:

A(a(f(b, a(x0)))) → c

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

a(a(f(b, a(z0)))) → f(a(a(a(z0))), b)
a(a(z0)) → f(b, a(f(a(z0), b)))
f(a(z0), b) → f(b, a(z0))
Tuples:

A(a(z0)) → c1(F(b, a(f(a(z0), b))), A(f(a(z0), b)), F(a(z0), b), A(z0))
F(a(z0), b) → c2(F(b, a(z0)), A(z0))
A(a(f(b, a(x0)))) → c(F(f(b, a(f(a(a(x0)), b))), b), A(a(a(x0))), A(a(x0)), A(x0))
A(a(f(b, a(f(b, a(z0)))))) → c(F(a(f(a(a(a(z0))), b)), b), A(a(a(f(b, a(z0))))), A(a(f(b, a(z0)))), A(f(b, a(z0))))
A(a(f(b, a(z0)))) → c(F(a(f(b, a(f(a(z0), b)))), b), A(a(a(z0))), A(a(z0)), A(z0))
S tuples:

A(a(z0)) → c1(F(b, a(f(a(z0), b))), A(f(a(z0), b)), F(a(z0), b), A(z0))
F(a(z0), b) → c2(F(b, a(z0)), A(z0))
A(a(f(b, a(x0)))) → c(F(f(b, a(f(a(a(x0)), b))), b), A(a(a(x0))), A(a(x0)), A(x0))
A(a(f(b, a(f(b, a(z0)))))) → c(F(a(f(a(a(a(z0))), b)), b), A(a(a(f(b, a(z0))))), A(a(f(b, a(z0)))), A(f(b, a(z0))))
A(a(f(b, a(z0)))) → c(F(a(f(b, a(f(a(z0), b)))), b), A(a(a(z0))), A(a(z0)), A(z0))
K tuples:none
Defined Rule Symbols:

a, f

Defined Pair Symbols:

A, F

Compound Symbols:

c1, c2, c

(7) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace A(a(z0)) → c1(F(b, a(f(a(z0), b))), A(f(a(z0), b)), F(a(z0), b), A(z0)) by

A(a(z0)) → c1(F(b, a(f(b, a(z0)))), A(f(a(z0), b)), F(a(z0), b), A(z0))
A(a(x0)) → c1

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

a(a(f(b, a(z0)))) → f(a(a(a(z0))), b)
a(a(z0)) → f(b, a(f(a(z0), b)))
f(a(z0), b) → f(b, a(z0))
Tuples:

F(a(z0), b) → c2(F(b, a(z0)), A(z0))
A(a(f(b, a(x0)))) → c(F(f(b, a(f(a(a(x0)), b))), b), A(a(a(x0))), A(a(x0)), A(x0))
A(a(f(b, a(f(b, a(z0)))))) → c(F(a(f(a(a(a(z0))), b)), b), A(a(a(f(b, a(z0))))), A(a(f(b, a(z0)))), A(f(b, a(z0))))
A(a(f(b, a(z0)))) → c(F(a(f(b, a(f(a(z0), b)))), b), A(a(a(z0))), A(a(z0)), A(z0))
A(a(z0)) → c1(F(b, a(f(b, a(z0)))), A(f(a(z0), b)), F(a(z0), b), A(z0))
A(a(x0)) → c1
S tuples:

F(a(z0), b) → c2(F(b, a(z0)), A(z0))
A(a(f(b, a(x0)))) → c(F(f(b, a(f(a(a(x0)), b))), b), A(a(a(x0))), A(a(x0)), A(x0))
A(a(f(b, a(f(b, a(z0)))))) → c(F(a(f(a(a(a(z0))), b)), b), A(a(a(f(b, a(z0))))), A(a(f(b, a(z0)))), A(f(b, a(z0))))
A(a(f(b, a(z0)))) → c(F(a(f(b, a(f(a(z0), b)))), b), A(a(a(z0))), A(a(z0)), A(z0))
A(a(z0)) → c1(F(b, a(f(b, a(z0)))), A(f(a(z0), b)), F(a(z0), b), A(z0))
A(a(x0)) → c1
K tuples:none
Defined Rule Symbols:

a, f

Defined Pair Symbols:

F, A

Compound Symbols:

c2, c, c1, c1

(9) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

Removed 1 trailing nodes:

A(a(x0)) → c1

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

a(a(f(b, a(z0)))) → f(a(a(a(z0))), b)
a(a(z0)) → f(b, a(f(a(z0), b)))
f(a(z0), b) → f(b, a(z0))
Tuples:

F(a(z0), b) → c2(F(b, a(z0)), A(z0))
A(a(f(b, a(x0)))) → c(F(f(b, a(f(a(a(x0)), b))), b), A(a(a(x0))), A(a(x0)), A(x0))
A(a(f(b, a(f(b, a(z0)))))) → c(F(a(f(a(a(a(z0))), b)), b), A(a(a(f(b, a(z0))))), A(a(f(b, a(z0)))), A(f(b, a(z0))))
A(a(f(b, a(z0)))) → c(F(a(f(b, a(f(a(z0), b)))), b), A(a(a(z0))), A(a(z0)), A(z0))
A(a(z0)) → c1(F(b, a(f(b, a(z0)))), A(f(a(z0), b)), F(a(z0), b), A(z0))
S tuples:

F(a(z0), b) → c2(F(b, a(z0)), A(z0))
A(a(f(b, a(x0)))) → c(F(f(b, a(f(a(a(x0)), b))), b), A(a(a(x0))), A(a(x0)), A(x0))
A(a(f(b, a(f(b, a(z0)))))) → c(F(a(f(a(a(a(z0))), b)), b), A(a(a(f(b, a(z0))))), A(a(f(b, a(z0)))), A(f(b, a(z0))))
A(a(f(b, a(z0)))) → c(F(a(f(b, a(f(a(z0), b)))), b), A(a(a(z0))), A(a(z0)), A(z0))
A(a(z0)) → c1(F(b, a(f(b, a(z0)))), A(f(a(z0), b)), F(a(z0), b), A(z0))
K tuples:none
Defined Rule Symbols:

a, f

Defined Pair Symbols:

F, A

Compound Symbols:

c2, c, c1

(11) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace F(a(z0), b) → c2(F(b, a(z0)), A(z0)) by

F(a(x0), b) → c2(A(x0))

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

a(a(f(b, a(z0)))) → f(a(a(a(z0))), b)
a(a(z0)) → f(b, a(f(a(z0), b)))
f(a(z0), b) → f(b, a(z0))
Tuples:

A(a(f(b, a(x0)))) → c(F(f(b, a(f(a(a(x0)), b))), b), A(a(a(x0))), A(a(x0)), A(x0))
A(a(f(b, a(f(b, a(z0)))))) → c(F(a(f(a(a(a(z0))), b)), b), A(a(a(f(b, a(z0))))), A(a(f(b, a(z0)))), A(f(b, a(z0))))
A(a(f(b, a(z0)))) → c(F(a(f(b, a(f(a(z0), b)))), b), A(a(a(z0))), A(a(z0)), A(z0))
A(a(z0)) → c1(F(b, a(f(b, a(z0)))), A(f(a(z0), b)), F(a(z0), b), A(z0))
F(a(x0), b) → c2(A(x0))
S tuples:

A(a(f(b, a(x0)))) → c(F(f(b, a(f(a(a(x0)), b))), b), A(a(a(x0))), A(a(x0)), A(x0))
A(a(f(b, a(f(b, a(z0)))))) → c(F(a(f(a(a(a(z0))), b)), b), A(a(a(f(b, a(z0))))), A(a(f(b, a(z0)))), A(f(b, a(z0))))
A(a(f(b, a(z0)))) → c(F(a(f(b, a(f(a(z0), b)))), b), A(a(a(z0))), A(a(z0)), A(z0))
A(a(z0)) → c1(F(b, a(f(b, a(z0)))), A(f(a(z0), b)), F(a(z0), b), A(z0))
F(a(x0), b) → c2(A(x0))
K tuples:none
Defined Rule Symbols:

a, f

Defined Pair Symbols:

A, F

Compound Symbols:

c, c1, c2

(13) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace A(a(f(b, a(x0)))) → c(F(f(b, a(f(a(a(x0)), b))), b), A(a(a(x0))), A(a(x0)), A(x0)) by

A(a(f(b, a(x0)))) → c(F(f(b, a(f(b, a(a(x0))))), b), A(a(a(x0))), A(a(x0)), A(x0))
A(a(f(b, a(f(b, a(z0)))))) → c(F(f(b, a(f(f(a(a(a(z0))), b), b))), b), A(a(a(f(b, a(z0))))), A(a(f(b, a(z0)))), A(f(b, a(z0))))
A(a(f(b, a(z0)))) → c(F(f(b, a(f(f(b, a(f(a(z0), b))), b))), b), A(a(a(z0))), A(a(z0)), A(z0))
A(a(f(b, a(x0)))) → c

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

a(a(f(b, a(z0)))) → f(a(a(a(z0))), b)
a(a(z0)) → f(b, a(f(a(z0), b)))
f(a(z0), b) → f(b, a(z0))
Tuples:

A(a(f(b, a(f(b, a(z0)))))) → c(F(a(f(a(a(a(z0))), b)), b), A(a(a(f(b, a(z0))))), A(a(f(b, a(z0)))), A(f(b, a(z0))))
A(a(f(b, a(z0)))) → c(F(a(f(b, a(f(a(z0), b)))), b), A(a(a(z0))), A(a(z0)), A(z0))
A(a(z0)) → c1(F(b, a(f(b, a(z0)))), A(f(a(z0), b)), F(a(z0), b), A(z0))
F(a(x0), b) → c2(A(x0))
A(a(f(b, a(x0)))) → c(F(f(b, a(f(b, a(a(x0))))), b), A(a(a(x0))), A(a(x0)), A(x0))
A(a(f(b, a(f(b, a(z0)))))) → c(F(f(b, a(f(f(a(a(a(z0))), b), b))), b), A(a(a(f(b, a(z0))))), A(a(f(b, a(z0)))), A(f(b, a(z0))))
A(a(f(b, a(z0)))) → c(F(f(b, a(f(f(b, a(f(a(z0), b))), b))), b), A(a(a(z0))), A(a(z0)), A(z0))
A(a(f(b, a(x0)))) → c
S tuples:

A(a(f(b, a(f(b, a(z0)))))) → c(F(a(f(a(a(a(z0))), b)), b), A(a(a(f(b, a(z0))))), A(a(f(b, a(z0)))), A(f(b, a(z0))))
A(a(f(b, a(z0)))) → c(F(a(f(b, a(f(a(z0), b)))), b), A(a(a(z0))), A(a(z0)), A(z0))
A(a(z0)) → c1(F(b, a(f(b, a(z0)))), A(f(a(z0), b)), F(a(z0), b), A(z0))
F(a(x0), b) → c2(A(x0))
A(a(f(b, a(x0)))) → c(F(f(b, a(f(b, a(a(x0))))), b), A(a(a(x0))), A(a(x0)), A(x0))
A(a(f(b, a(f(b, a(z0)))))) → c(F(f(b, a(f(f(a(a(a(z0))), b), b))), b), A(a(a(f(b, a(z0))))), A(a(f(b, a(z0)))), A(f(b, a(z0))))
A(a(f(b, a(z0)))) → c(F(f(b, a(f(f(b, a(f(a(z0), b))), b))), b), A(a(a(z0))), A(a(z0)), A(z0))
A(a(f(b, a(x0)))) → c
K tuples:none
Defined Rule Symbols:

a, f

Defined Pair Symbols:

A, F

Compound Symbols:

c, c1, c2, c

(15) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

Removed 1 trailing nodes:

A(a(f(b, a(x0)))) → c

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

a(a(f(b, a(z0)))) → f(a(a(a(z0))), b)
a(a(z0)) → f(b, a(f(a(z0), b)))
f(a(z0), b) → f(b, a(z0))
Tuples:

A(a(f(b, a(f(b, a(z0)))))) → c(F(a(f(a(a(a(z0))), b)), b), A(a(a(f(b, a(z0))))), A(a(f(b, a(z0)))), A(f(b, a(z0))))
A(a(f(b, a(z0)))) → c(F(a(f(b, a(f(a(z0), b)))), b), A(a(a(z0))), A(a(z0)), A(z0))
A(a(z0)) → c1(F(b, a(f(b, a(z0)))), A(f(a(z0), b)), F(a(z0), b), A(z0))
F(a(x0), b) → c2(A(x0))
A(a(f(b, a(x0)))) → c(F(f(b, a(f(b, a(a(x0))))), b), A(a(a(x0))), A(a(x0)), A(x0))
A(a(f(b, a(f(b, a(z0)))))) → c(F(f(b, a(f(f(a(a(a(z0))), b), b))), b), A(a(a(f(b, a(z0))))), A(a(f(b, a(z0)))), A(f(b, a(z0))))
A(a(f(b, a(z0)))) → c(F(f(b, a(f(f(b, a(f(a(z0), b))), b))), b), A(a(a(z0))), A(a(z0)), A(z0))
S tuples:

A(a(f(b, a(f(b, a(z0)))))) → c(F(a(f(a(a(a(z0))), b)), b), A(a(a(f(b, a(z0))))), A(a(f(b, a(z0)))), A(f(b, a(z0))))
A(a(f(b, a(z0)))) → c(F(a(f(b, a(f(a(z0), b)))), b), A(a(a(z0))), A(a(z0)), A(z0))
A(a(z0)) → c1(F(b, a(f(b, a(z0)))), A(f(a(z0), b)), F(a(z0), b), A(z0))
F(a(x0), b) → c2(A(x0))
A(a(f(b, a(x0)))) → c(F(f(b, a(f(b, a(a(x0))))), b), A(a(a(x0))), A(a(x0)), A(x0))
A(a(f(b, a(f(b, a(z0)))))) → c(F(f(b, a(f(f(a(a(a(z0))), b), b))), b), A(a(a(f(b, a(z0))))), A(a(f(b, a(z0)))), A(f(b, a(z0))))
A(a(f(b, a(z0)))) → c(F(f(b, a(f(f(b, a(f(a(z0), b))), b))), b), A(a(a(z0))), A(a(z0)), A(z0))
K tuples:none
Defined Rule Symbols:

a, f

Defined Pair Symbols:

A, F

Compound Symbols:

c, c1, c2

(17) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace A(a(f(b, a(f(b, a(z0)))))) → c(F(a(f(a(a(a(z0))), b)), b), A(a(a(f(b, a(z0))))), A(a(f(b, a(z0)))), A(f(b, a(z0)))) by

A(a(f(b, a(f(b, a(x0)))))) → c(F(a(f(b, a(a(a(x0))))), b), A(a(a(f(b, a(x0))))), A(a(f(b, a(x0)))), A(f(b, a(x0))))
A(a(f(b, a(f(b, a(x0)))))) → c(F(a(f(f(b, a(f(a(a(x0)), b))), b)), b), A(a(a(f(b, a(x0))))), A(a(f(b, a(x0)))), A(f(b, a(x0))))
A(a(f(b, a(f(b, a(f(b, a(z0)))))))) → c(F(a(f(a(f(a(a(a(z0))), b)), b)), b), A(a(a(f(b, a(f(b, a(z0))))))), A(a(f(b, a(f(b, a(z0)))))), A(f(b, a(f(b, a(z0))))))
A(a(f(b, a(f(b, a(z0)))))) → c(F(a(f(a(f(b, a(f(a(z0), b)))), b)), b), A(a(a(f(b, a(z0))))), A(a(f(b, a(z0)))), A(f(b, a(z0))))
A(a(f(b, a(f(b, a(x0)))))) → c(A(a(a(f(b, a(x0))))), A(a(f(b, a(x0)))))

(18) Obligation:

Complexity Dependency Tuples Problem
Rules:

a(a(f(b, a(z0)))) → f(a(a(a(z0))), b)
a(a(z0)) → f(b, a(f(a(z0), b)))
f(a(z0), b) → f(b, a(z0))
Tuples:

A(a(f(b, a(z0)))) → c(F(a(f(b, a(f(a(z0), b)))), b), A(a(a(z0))), A(a(z0)), A(z0))
A(a(z0)) → c1(F(b, a(f(b, a(z0)))), A(f(a(z0), b)), F(a(z0), b), A(z0))
F(a(x0), b) → c2(A(x0))
A(a(f(b, a(x0)))) → c(F(f(b, a(f(b, a(a(x0))))), b), A(a(a(x0))), A(a(x0)), A(x0))
A(a(f(b, a(f(b, a(z0)))))) → c(F(f(b, a(f(f(a(a(a(z0))), b), b))), b), A(a(a(f(b, a(z0))))), A(a(f(b, a(z0)))), A(f(b, a(z0))))
A(a(f(b, a(z0)))) → c(F(f(b, a(f(f(b, a(f(a(z0), b))), b))), b), A(a(a(z0))), A(a(z0)), A(z0))
A(a(f(b, a(f(b, a(x0)))))) → c(F(a(f(b, a(a(a(x0))))), b), A(a(a(f(b, a(x0))))), A(a(f(b, a(x0)))), A(f(b, a(x0))))
A(a(f(b, a(f(b, a(x0)))))) → c(F(a(f(f(b, a(f(a(a(x0)), b))), b)), b), A(a(a(f(b, a(x0))))), A(a(f(b, a(x0)))), A(f(b, a(x0))))
A(a(f(b, a(f(b, a(f(b, a(z0)))))))) → c(F(a(f(a(f(a(a(a(z0))), b)), b)), b), A(a(a(f(b, a(f(b, a(z0))))))), A(a(f(b, a(f(b, a(z0)))))), A(f(b, a(f(b, a(z0))))))
A(a(f(b, a(f(b, a(z0)))))) → c(F(a(f(a(f(b, a(f(a(z0), b)))), b)), b), A(a(a(f(b, a(z0))))), A(a(f(b, a(z0)))), A(f(b, a(z0))))
A(a(f(b, a(f(b, a(x0)))))) → c(A(a(a(f(b, a(x0))))), A(a(f(b, a(x0)))))
S tuples:

A(a(f(b, a(z0)))) → c(F(a(f(b, a(f(a(z0), b)))), b), A(a(a(z0))), A(a(z0)), A(z0))
A(a(z0)) → c1(F(b, a(f(b, a(z0)))), A(f(a(z0), b)), F(a(z0), b), A(z0))
F(a(x0), b) → c2(A(x0))
A(a(f(b, a(x0)))) → c(F(f(b, a(f(b, a(a(x0))))), b), A(a(a(x0))), A(a(x0)), A(x0))
A(a(f(b, a(f(b, a(z0)))))) → c(F(f(b, a(f(f(a(a(a(z0))), b), b))), b), A(a(a(f(b, a(z0))))), A(a(f(b, a(z0)))), A(f(b, a(z0))))
A(a(f(b, a(z0)))) → c(F(f(b, a(f(f(b, a(f(a(z0), b))), b))), b), A(a(a(z0))), A(a(z0)), A(z0))
A(a(f(b, a(f(b, a(x0)))))) → c(F(a(f(b, a(a(a(x0))))), b), A(a(a(f(b, a(x0))))), A(a(f(b, a(x0)))), A(f(b, a(x0))))
A(a(f(b, a(f(b, a(x0)))))) → c(F(a(f(f(b, a(f(a(a(x0)), b))), b)), b), A(a(a(f(b, a(x0))))), A(a(f(b, a(x0)))), A(f(b, a(x0))))
A(a(f(b, a(f(b, a(f(b, a(z0)))))))) → c(F(a(f(a(f(a(a(a(z0))), b)), b)), b), A(a(a(f(b, a(f(b, a(z0))))))), A(a(f(b, a(f(b, a(z0)))))), A(f(b, a(f(b, a(z0))))))
A(a(f(b, a(f(b, a(z0)))))) → c(F(a(f(a(f(b, a(f(a(z0), b)))), b)), b), A(a(a(f(b, a(z0))))), A(a(f(b, a(z0)))), A(f(b, a(z0))))
A(a(f(b, a(f(b, a(x0)))))) → c(A(a(a(f(b, a(x0))))), A(a(f(b, a(x0)))))
K tuples:none
Defined Rule Symbols:

a, f

Defined Pair Symbols:

A, F

Compound Symbols:

c, c1, c2, c

(19) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace A(a(f(b, a(z0)))) → c(F(a(f(b, a(f(a(z0), b)))), b), A(a(a(z0))), A(a(z0)), A(z0)) by

A(a(f(b, a(z0)))) → c(F(a(f(b, a(f(b, a(z0))))), b), A(a(a(z0))), A(a(z0)), A(z0))
A(a(f(b, a(x0)))) → c(A(a(a(x0))))

(20) Obligation:

Complexity Dependency Tuples Problem
Rules:

a(a(f(b, a(z0)))) → f(a(a(a(z0))), b)
a(a(z0)) → f(b, a(f(a(z0), b)))
f(a(z0), b) → f(b, a(z0))
Tuples:

A(a(z0)) → c1(F(b, a(f(b, a(z0)))), A(f(a(z0), b)), F(a(z0), b), A(z0))
F(a(x0), b) → c2(A(x0))
A(a(f(b, a(x0)))) → c(F(f(b, a(f(b, a(a(x0))))), b), A(a(a(x0))), A(a(x0)), A(x0))
A(a(f(b, a(f(b, a(z0)))))) → c(F(f(b, a(f(f(a(a(a(z0))), b), b))), b), A(a(a(f(b, a(z0))))), A(a(f(b, a(z0)))), A(f(b, a(z0))))
A(a(f(b, a(z0)))) → c(F(f(b, a(f(f(b, a(f(a(z0), b))), b))), b), A(a(a(z0))), A(a(z0)), A(z0))
A(a(f(b, a(f(b, a(x0)))))) → c(F(a(f(b, a(a(a(x0))))), b), A(a(a(f(b, a(x0))))), A(a(f(b, a(x0)))), A(f(b, a(x0))))
A(a(f(b, a(f(b, a(x0)))))) → c(F(a(f(f(b, a(f(a(a(x0)), b))), b)), b), A(a(a(f(b, a(x0))))), A(a(f(b, a(x0)))), A(f(b, a(x0))))
A(a(f(b, a(f(b, a(f(b, a(z0)))))))) → c(F(a(f(a(f(a(a(a(z0))), b)), b)), b), A(a(a(f(b, a(f(b, a(z0))))))), A(a(f(b, a(f(b, a(z0)))))), A(f(b, a(f(b, a(z0))))))
A(a(f(b, a(f(b, a(z0)))))) → c(F(a(f(a(f(b, a(f(a(z0), b)))), b)), b), A(a(a(f(b, a(z0))))), A(a(f(b, a(z0)))), A(f(b, a(z0))))
A(a(f(b, a(f(b, a(x0)))))) → c(A(a(a(f(b, a(x0))))), A(a(f(b, a(x0)))))
A(a(f(b, a(z0)))) → c(F(a(f(b, a(f(b, a(z0))))), b), A(a(a(z0))), A(a(z0)), A(z0))
A(a(f(b, a(x0)))) → c(A(a(a(x0))))
S tuples:

A(a(z0)) → c1(F(b, a(f(b, a(z0)))), A(f(a(z0), b)), F(a(z0), b), A(z0))
F(a(x0), b) → c2(A(x0))
A(a(f(b, a(x0)))) → c(F(f(b, a(f(b, a(a(x0))))), b), A(a(a(x0))), A(a(x0)), A(x0))
A(a(f(b, a(f(b, a(z0)))))) → c(F(f(b, a(f(f(a(a(a(z0))), b), b))), b), A(a(a(f(b, a(z0))))), A(a(f(b, a(z0)))), A(f(b, a(z0))))
A(a(f(b, a(z0)))) → c(F(f(b, a(f(f(b, a(f(a(z0), b))), b))), b), A(a(a(z0))), A(a(z0)), A(z0))
A(a(f(b, a(f(b, a(x0)))))) → c(F(a(f(b, a(a(a(x0))))), b), A(a(a(f(b, a(x0))))), A(a(f(b, a(x0)))), A(f(b, a(x0))))
A(a(f(b, a(f(b, a(x0)))))) → c(F(a(f(f(b, a(f(a(a(x0)), b))), b)), b), A(a(a(f(b, a(x0))))), A(a(f(b, a(x0)))), A(f(b, a(x0))))
A(a(f(b, a(f(b, a(f(b, a(z0)))))))) → c(F(a(f(a(f(a(a(a(z0))), b)), b)), b), A(a(a(f(b, a(f(b, a(z0))))))), A(a(f(b, a(f(b, a(z0)))))), A(f(b, a(f(b, a(z0))))))
A(a(f(b, a(f(b, a(z0)))))) → c(F(a(f(a(f(b, a(f(a(z0), b)))), b)), b), A(a(a(f(b, a(z0))))), A(a(f(b, a(z0)))), A(f(b, a(z0))))
A(a(f(b, a(f(b, a(x0)))))) → c(A(a(a(f(b, a(x0))))), A(a(f(b, a(x0)))))
A(a(f(b, a(z0)))) → c(F(a(f(b, a(f(b, a(z0))))), b), A(a(a(z0))), A(a(z0)), A(z0))
A(a(f(b, a(x0)))) → c(A(a(a(x0))))
K tuples:none
Defined Rule Symbols:

a, f

Defined Pair Symbols:

A, F

Compound Symbols:

c1, c2, c, c, c

(21) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace A(a(z0)) → c1(F(b, a(f(b, a(z0)))), A(f(a(z0), b)), F(a(z0), b), A(z0)) by

A(a(x0)) → c1(A(f(a(x0), b)), F(a(x0), b), A(x0))

(22) Obligation:

Complexity Dependency Tuples Problem
Rules:

a(a(f(b, a(z0)))) → f(a(a(a(z0))), b)
a(a(z0)) → f(b, a(f(a(z0), b)))
f(a(z0), b) → f(b, a(z0))
Tuples:

F(a(x0), b) → c2(A(x0))
A(a(f(b, a(x0)))) → c(F(f(b, a(f(b, a(a(x0))))), b), A(a(a(x0))), A(a(x0)), A(x0))
A(a(f(b, a(f(b, a(z0)))))) → c(F(f(b, a(f(f(a(a(a(z0))), b), b))), b), A(a(a(f(b, a(z0))))), A(a(f(b, a(z0)))), A(f(b, a(z0))))
A(a(f(b, a(z0)))) → c(F(f(b, a(f(f(b, a(f(a(z0), b))), b))), b), A(a(a(z0))), A(a(z0)), A(z0))
A(a(f(b, a(f(b, a(x0)))))) → c(F(a(f(b, a(a(a(x0))))), b), A(a(a(f(b, a(x0))))), A(a(f(b, a(x0)))), A(f(b, a(x0))))
A(a(f(b, a(f(b, a(x0)))))) → c(F(a(f(f(b, a(f(a(a(x0)), b))), b)), b), A(a(a(f(b, a(x0))))), A(a(f(b, a(x0)))), A(f(b, a(x0))))
A(a(f(b, a(f(b, a(f(b, a(z0)))))))) → c(F(a(f(a(f(a(a(a(z0))), b)), b)), b), A(a(a(f(b, a(f(b, a(z0))))))), A(a(f(b, a(f(b, a(z0)))))), A(f(b, a(f(b, a(z0))))))
A(a(f(b, a(f(b, a(z0)))))) → c(F(a(f(a(f(b, a(f(a(z0), b)))), b)), b), A(a(a(f(b, a(z0))))), A(a(f(b, a(z0)))), A(f(b, a(z0))))
A(a(f(b, a(f(b, a(x0)))))) → c(A(a(a(f(b, a(x0))))), A(a(f(b, a(x0)))))
A(a(f(b, a(z0)))) → c(F(a(f(b, a(f(b, a(z0))))), b), A(a(a(z0))), A(a(z0)), A(z0))
A(a(f(b, a(x0)))) → c(A(a(a(x0))))
A(a(x0)) → c1(A(f(a(x0), b)), F(a(x0), b), A(x0))
S tuples:

F(a(x0), b) → c2(A(x0))
A(a(f(b, a(x0)))) → c(F(f(b, a(f(b, a(a(x0))))), b), A(a(a(x0))), A(a(x0)), A(x0))
A(a(f(b, a(f(b, a(z0)))))) → c(F(f(b, a(f(f(a(a(a(z0))), b), b))), b), A(a(a(f(b, a(z0))))), A(a(f(b, a(z0)))), A(f(b, a(z0))))
A(a(f(b, a(z0)))) → c(F(f(b, a(f(f(b, a(f(a(z0), b))), b))), b), A(a(a(z0))), A(a(z0)), A(z0))
A(a(f(b, a(f(b, a(x0)))))) → c(F(a(f(b, a(a(a(x0))))), b), A(a(a(f(b, a(x0))))), A(a(f(b, a(x0)))), A(f(b, a(x0))))
A(a(f(b, a(f(b, a(x0)))))) → c(F(a(f(f(b, a(f(a(a(x0)), b))), b)), b), A(a(a(f(b, a(x0))))), A(a(f(b, a(x0)))), A(f(b, a(x0))))
A(a(f(b, a(f(b, a(f(b, a(z0)))))))) → c(F(a(f(a(f(a(a(a(z0))), b)), b)), b), A(a(a(f(b, a(f(b, a(z0))))))), A(a(f(b, a(f(b, a(z0)))))), A(f(b, a(f(b, a(z0))))))
A(a(f(b, a(f(b, a(z0)))))) → c(F(a(f(a(f(b, a(f(a(z0), b)))), b)), b), A(a(a(f(b, a(z0))))), A(a(f(b, a(z0)))), A(f(b, a(z0))))
A(a(f(b, a(f(b, a(x0)))))) → c(A(a(a(f(b, a(x0))))), A(a(f(b, a(x0)))))
A(a(f(b, a(z0)))) → c(F(a(f(b, a(f(b, a(z0))))), b), A(a(a(z0))), A(a(z0)), A(z0))
A(a(f(b, a(x0)))) → c(A(a(a(x0))))
A(a(x0)) → c1(A(f(a(x0), b)), F(a(x0), b), A(x0))
K tuples:none
Defined Rule Symbols:

a, f

Defined Pair Symbols:

F, A

Compound Symbols:

c2, c, c, c, c1

(23) CpxTrsMatchBoundsTAProof (EQUIVALENT transformation)

A linear upper bound on the runtime complexity of the TRS R could be shown with a Match-Bound[TAB_LEFTLINEAR,TAB_NONLEFTLINEAR] (for contructor-based start-terms) of 0.

The compatible tree automaton used to show the Match-Boundedness (for constructor-based start-terms) is represented by:
final states : [1, 2]
transitions:
b0() → 0
a0(0) → 1
f0(0, 0) → 2

(24) BOUNDS(O(1), O(n^1))